package at.fhj.ase;

public class Buffer implements Cloneable {

	protected int in,out;
	protected Object[] buf;

	public Buffer() {
		buf = new Object[0];
	}

	public Buffer (int anzahl) {
		/** require anzahl > 0; **/
		buf = new Object[anzahl];
		/** ensure buf.length == anzahl; **/
	}

	public boolean empty() {
		return in - out == 0;
		/** ensure changeonly{}; **/
	}

	public boolean full() {
		return in - out == buf.length;
		/** ensure changeonly{}; **/    
	}

	public void add(Object o) {
		/** require [valid_object] o != null; [buffer_not_full] !full(); **/
		buf[in % buf.length] = o;
		in++;
		/** ensure changeonly{in,buf}; Old.in == in - 1; **/
	}

	public Object remove() {
		/** require [buffer_not_empty] !empty(); **/
		Object o = buf[out % buf.length];
		out++;
		return o;
		/** ensure changeonly{out}; [valid_object] Result != null; **/
	} 

	public boolean contains(Object o) {
		/** require o != null; **/
		boolean found = false;
		for (int i = 0; i < buf.length; i++) 
			/** invariant 0 <= i && i <= buf.length; **/
			/** variant buf.length - i **/
			if (buf[i].equals(o)) 
				found = true;
		return found;
		/** ensure changeonly{}; **/    
	}   

	protected Object clone() {
		/* Use the Objects clone method. This is enough cause only in and out 
		       are refered with Old expressions. */
		Object b = null;
		try {
			b = super.clone();
		}     
		catch (CloneNotSupportedException e){;}
		return b;
	}

	/** invariant [range] 0 <= in - out && in - out <= buf.length; 
		        [valid_content] buf.length == 0 || 
			   (forall i : {out%buf.length .. in%buf.length-1} # buf[i] != null);
	 **/
}
